$\forall$${\it es}$:ES, $A$:Type, ${\it Ias}$:(AbsInterface($A$) List), $e$:E.
\\[0ex]($\uparrow$($e$ $\in_{b}$ p{-}first(${\it Ias}$))) $\Leftarrow\!\Rightarrow$ ($\exists$$I$$\in$${\it Ias}$.$\uparrow$($e$ $\in_{b}$ $I$))